Inference at * 
Iof proof for Lemma sub-equality:


  T:Type, P:(T), i, u:T. (i = u)  (P(u))  (i = u) 

latex

 by Auto 

latex

 1: 

 1: 1. T : Type
 1: 2. P : T
 1: 3. i : T
 1: 4. u : T
 1: 5. i = u
 1: 6. P(u)
 1:   i = u
 .

Definitions

P  Q, {x:A| B(x)} , x:A. B(x), f(a), x:AB(x), , s = t, t  T, Type